a, b1, b2:. CoPrime(a,b1)  CoPrime(a,b2)  CoPrime(a,b1b2) 

latex

Definitions	P  Q, CoPrime(a,b), x:A. B(x), t  T, P  Q, P & Q, P  Q, x:A. B(x), Prop
Lemmas	mul functionality wrt eq, add mono wrt eq, coprime bezout id, coprime wf